Lambda the Ultimate

http://www.malevole.com/mv/misc/killerquiz/

Simon Peyton Jones has a new paper about type inferencing and GADT's: Simple unification-based type inference for GADTs

Generalized algebraic data types (GADTs), sometimes known as "guarded recursive data types" or "first-class phantom types", are a simple but powerful generalization of the data types of Haskell and ML. Recent works have given compelling examples of the utility of GADTs, although type inference is known to be difficult. Our contribution is to show how to exploit programmer-supplied type annotations to make the type inference task almost embarrassingly easy. Our main technical innovation is wobbly types, which express in a declarative way the uncertainty caused by the incremental nature of typical type-inference algorithms.

This paper is a much simplified and completely-rewritten version of his earlier paper Wobbly types: type inference for generalised algebraic data types

In my eternal quest for provably safe concurrent and distributed resource management, I'm trying to reach an understanding of dependent types. I have read a bit about them, even toyed a little bit with them in Twelf, but I still don't quite *get* them.

• Really, what *are* dependent types ? What do we expect to do with them ? Where exactly does the domain stop ?
• Have DML, Cayenne, Epigram been tested with pragmatic examples, beyond simple lists manipulation ? -- I don't include Twelf or Coq in the list as the focus of these languages is quite different.
• What are the limitations of dependent types ? Is typechecking even decidable ?
• How much of dependent typing can be encoded with non-dependent types ?
• Are there works on dynamic counterparts of dependent types ?
• What papers/tutorials must one absolutely read on the subject ?

By the way, the Wikipedia article on Dependent Types is nearly empty. Is there anyone interested in completing it ?

Been reading LtU for a while and some of the topics discussed have encouraged me to try using some of the more advanced functions supported by JavaScript. I'm pretty sure I'm using closures, but had a few questions-

js closures?

...so my questions are:

If the form is:

someId = window.setInterval( ... );

...is there a way to pass someId back into the function that was created? In OO terms, something like the following:

closure = new SomeThingy();
someId = window.setInterval( closure, 1000 );
closure.setSomeExtraValue( someId );

...and is the explanation in the blog post fairly accurate?

Thanks!

--Robert

The Fortress specs have been updated.

http://research.sun.com/projects/plrg/fortress0785.pdf

A very interesting thesis, by Holger Gast, at
http://www-pu.informatik.uni-tuebingen.de/users/gast/tcg.html.

From the abstract :
This thesis presents a generator for type checkers. Given a description of the type system by typing rules, the generator yields a type checker that constructs proofs using the typing rules. Unlike earlier approaches, we derive suitable notions of proof and typing rule from an analysis of type systems and from corresponding constructs in mathematical proof theory. The approach thus respects the structure and intention of the typing rules, rather than expressing the rules in some pre-existing formalism.

I hope that TCG will be released soon.

"Algebra Of Programming" has been mentioned on LTU a few times (mostly in 2002 it seems). Unfortunately the book is not available on-line, and costs $125 on Amazon! Since the book is about 9 years old now, I'm wondering if there are is any other material that summarizes it, re-states it or supersedes it?

Secondly, from what I have read, the examples in the book are in haskell, should I expect any problems if I use Scheme to implement those examples?

Neko 1.1 have just been released at http://nekovm.org.

Neko is an intermediate programming language. It has been designed to provide a common runtime for several different languages.

In this new version, the compiler is now completely bootstrapped, using the high level NekoML language which itself use Neko for its runtime. A toplevel console is also available and the VM has new features such as callstack and exception stack traces.

I'm looking for people interesting in targeting Neko or doing some study of the principles behind it. Please feel free to send me an email or join the Neko Mailing List if interested.

As always, comments and critics are welcome.

Nicolas

I grew up with Pascal. It's been my language of choice for doing mostly everything. Everytime I try and switch to other (case sensitive) languages, specifically C++/C#, I am incredibly put off by the case sensitivity of the syntax.

What especially gets me, especially from a readability point of view, are things like variable declarations in the following fashion:


TD_SOMETYPE td_sometype;


That's the most braindead thing I've ever seen, naming a variable after the type, except it's unique because the character case is different....

Not only does this kill readability, but the very nature of the case sensitive syntax means that you're constantly having to think about variable names, instead of just using the bloody things in that activity otherwise known as programming.

And don't get me started on the debugging headaches it causes simply because you typed "S" instead of "s", somewhere. To me, it makes the coding process needlessly complicated.

The ordinal value of a character shouldn't change its meaning except if it specifically occurs as data. Of course, the source code of a program IS data, but only for use by the compiler. Why should we as programmers have to suffer just to keep the compiler happy?

Somebody, please give me some good solid reasons why case-sensitivity is useful. M$ had a golden opportunity with C#, yet they kept it case-sensitive. WHY? Surely it wasn't to support existing code bases, was it?

The Role of Type Equality in Meta-Programming (Emir Pasalic)

Meta-programming, writing programs that write other programs, involves two kinds of languages. The meta-language is the language in which meta-programs, which construct or manipulate other programs, are written. The object-language is the language of programs being manipulated.
We study a class of meta-language features that are used to write meta-programs that are statically guaranteed to maintain semantic invariants of object-language programs, such as typing and scoping. We use type equality in the type system of the meta-language to check and enforce these invariants. Our main contribution is the illustration of the utility of type equality in typed functional meta-programming. In particular, we encode and capture judgments about many important language features using type equality.
Finally, we show how type equality is incorporated as a feature of the type system of a practical functional
meta-programming language.

An interesting investigation by Emir Pasalic into meta programming and its relation to both dependent typing and multi-stage programming, among which an exposé of the development of Omega (see also: Tim Sheard ).